Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		minus(x,0)	→ x
2:		minus(0,y)	→ 0
3:		minus(s(x),s(y))	→ minus(p(s(x)),p(s(y)))
4:		minus(x,plus(y,z))	→ minus(minus(x,y),z)
5:		p(s(s(x)))	→ s(p(s(x)))
6:		p(0)	→ s(s(0))
7:		div(s(x),s(y))	→ s(div(minus(x,y),s(y)))
8:		div(plus(x,y),z)	→ plus(div(x,z),div(y,z))
9:		plus(0,y)	→ y
10:		plus(s(x),y)	→ s(plus(y,minus(s(x),s(0))))

There are 13 dependency pairs:


11:		MINUS(s(x),s(y))	→ MINUS(p(s(x)),p(s(y)))
12:		MINUS(s(x),s(y))	→ P(s(x))
13:		MINUS(s(x),s(y))	→ P(s(y))
14:		MINUS(x,plus(y,z))	→ MINUS(minus(x,y),z)
15:		MINUS(x,plus(y,z))	→ MINUS(x,y)
16:		P(s(s(x)))	→ P(s(x))
17:		DIV(s(x),s(y))	→ DIV(minus(x,y),s(y))
18:		DIV(s(x),s(y))	→ MINUS(x,y)
19:		DIV(plus(x,y),z)	→ PLUS(div(x,z),div(y,z))
20:		DIV(plus(x,y),z)	→ DIV(x,z)
21:		DIV(plus(x,y),z)	→ DIV(y,z)
22:		PLUS(s(x),y)	→ PLUS(y,minus(s(x),s(0)))
23:		PLUS(s(x),y)	→ MINUS(s(x),s(0))

The approximated dependency graph contains 4 SCCs: {16}, {11,14,15}, {22} and {17,20,21}.

Consider the SCC {16}. There are no usable rules. By taking the AF π with π(P) = 1 together with the lexicographic path order with empty precedence, rule 16 is strictly decreasing.

Consider the SCC {11,14,15}. The usable rules are {1-6}. By taking the AF π with π(minus) = π(p) = π(s) = 1 and π(MINUS) = 2 together with the lexicographic path order with empty precedence, the rules in {1-6,11} are weakly decreasing and the rules in {14,15} are strictly decreasing. There is one new SCC.
- Consider the SCC {11}. The usable rules are {5,6}. The constraints could not be solved.

Consider the SCC {22}. The usable rules are {1-6}. The constraints could not be solved.

Consider the SCC {17,20,21}. The usable rules are {1-6}. By taking the AF π with π(DIV) = π(minus) = π(p) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {1-6,17} are weakly decreasing and the rules in {20,21} are strictly decreasing. There is one new SCC.
- Consider the SCC {17}. The constraints could not be solved.

Tyrolean Termination Tool (0.05 seconds) --- May 4, 2006